\section{M\'odulo Dados}

\subsection{Servicios Exportados}

\subsubsection{Interfaz \nombretad{Dados}}


\textbf{G\'enero:} dados

\textbf{Usa interfaces:}\\
\indent\indent \nombretad{Nat}, \nombretad{Bool}, \nombretad{Tupla}

\textbf{\bf se explica con especificacion:} \nombretad{Dados}

\vspace{0.5cm}

\textbf{Operaciones:}

\noindent
dados(in $n_1$: nat , in $n_2$: nat) $\rightarrow$ ret: dados \\
\{$ 1 \leq n_1 \geq 6 \land 1 \leq n_2 \geq 6 $\} \\
\{$ \sombrero{ret} = <n_1,n_2> $\} \\

\noindent
SonIguales(in d: dados) $\rightarrow$ ret: bool \\
\{ true \} \\
\{$ \sombrero{ret} = (\Pi_1(d) \igobs \Pi_2(d)) $\} \\

\noindent
Suma(in d: dados) $\rightarrow$ ret: bool \\
\{ true \} \\
\{$ \sombrero{ret} = (\Pi_1(d) + \Pi_2(d)) $\} \\

\vspace{0.5cm}

\subsubsection{Aspectos de Aliasing}
\begin{itemize}
\item No posee.
\end{itemize}

\subsubsection{Ordenes de Complejidad}

\begin{itemize}
\item SonIguales: $O(1)$
\item Suma: $O(1)$
\end{itemize}

\subsection{Representaci\'on}

\subsubsection{Estructura de Representaci\'on}
$dados$ src {\bf estrD} donde {\bf estrD} es

tupla ( n1 : Nat, n2 : Nat )

\subsubsection{Invariante de Representaci\'on}
Rep: $\sombrero{estrD}$ $\longrightarrow boolean $
$(\forall e: \sombrero{estrD})\,Rep(e) \equiv$

\begin{enumerate}
\item{$ (\forall d: dados)(2 \leq \Pi_1(d) \geq 6 \land 1 \leq \Pi_2(d) \geq 6 ) $} 
\end{enumerate}

\vspace{0.5cm}

\subsubsection{Explicaciones del Invariante}
\begin{enumerate}
\item{Los valores en la tupla son dados v\'alidos.}
\end{enumerate}
\vspace{0.3cm}

\subsubsection{Funci\'on de Abstracci\'on}

($\forall$ $e$: $\sombrero{estrD}$) Abs($e$)  $\equiv$ $d$: $\sombrero{dados}$ {\bf tal que} 

( $ Suma(d) = \Pi_1(estrD) + \Pi_2(estrD) $ \\ 
$ SonIguales(d) = \Pi_1(estrD) \igobs \Pi_2(estrD) $ )
\newpage

\subsubsection{Consideraciones sobre la elecci\'on de la estructura}
\vspace{0.2cm}
Teniendo en cuenta que  \textit{d: estrD} es nuestra estructura de representaci\'on, realizamos las siguientes consideraciones al elegir la estructura a utilizar: \\
\\
\textbf{Sobre la Estructura de Representaci\'on}
\begin{itemize}
\item{Es una tupla que representa ambos dados.}
\end{itemize}

\vspace{0.5cm}

\textbf{Elecci\'on de la estructura de representaci\'on}
\begin{itemize}
\item{Se opt\'o por guardar individualmente ambos dados (por sobre la alternativa de almacenar solamente la suma y el valor de verdad de la igualdad) debido a que, seg\'un las especificaciones del TAD es un dato externo y es mas natural que sea proporcionado de esta manera}
\end{itemize}


\subsection{Algoritmos}
%----------------------------------------------------------------------------------


\begin{algorithm}{\it iDados}{\param {in}{n_1}{nat}, \param {in}{n_2}{nat} }{res\!:dados}
	res \= <n_1,n_2>
\end{algorithm}

\vspace{0.5cm}

\begin{algorithm}{\it iSonIguales}{\param {in}{d}{dados}}{res\!:bool}
	res \= \Pi_1(d) = \Pi_2(d)
\end{algorithm}

\vspace{0.5cm}

\begin{algorithm}{\it iSuma}{\param {in}{d}{dados}}{res\!:nat}
	res \= \Pi_1(d) + \Pi_2(d)
\end{algorithm}

\vspace{0.5cm}

\newpage


\subsubsection{Explicaci\'on de los \'ordenes de complejidad }
\begin{itemize}

\item{SonIguales: El orden de esta funci\'on es $O(1)$, dado que consiste en comparar dos instancias del tipo \nombretad{Nat} guardados en una tupla.}

\item{SonIguales: El orden de esta funci\'on es $O(1)$, dado que consiste en sumar dos instancias del tipo \nombretad{Nat} guardados en una tupla.}

\end{itemize}


\subsection{Servicios Usados}
Para poder cumplir con los \'ordenes de complejidad requeridos, es necesario pedirle a los tipos usados los siguientes \'ordenes de complejidad para algunas funciones:

\subsubsection{\nombretad{Nat}}
\begin{itemize}
\item +: $O(1)$
\end{itemize}

\subsubsection{\nombretad{Tupla}}
\begin{itemize}
\item $\Pi_n$: $O(1)$
\end{itemize}

\newpage